Trait isotope::term::dynamic::DynamicValue[][src]

pub trait DynamicValue: Debug + Any + DynHash {
Show methods fn dyn_cons(&self, ctx: &mut dyn ConsCtx) -> Option<TermId>;
fn dyn_ty(&self) -> Option<AnnotationRef<'_>>;
fn dyn_ix(&self) -> Option<NodeIx>;
fn dyn_code(&self) -> Code;
fn dyn_is_local_ty(&self) -> Option<bool>;
fn dyn_is_local_universe(&self) -> Option<bool>;
fn dyn_is_root(&self) -> bool;
fn dyn_is_subtype_in(
        &self,
        other: &Term,
        ctx: &mut dyn TermEqCtxMut
    ) -> Option<bool>;
fn dyn_universe(&self) -> Option<Universe>;
fn dyn_untyped_code(&self) -> Code;
fn dyn_filter(&self) -> VarFilter;
fn dyn_shift(
        &self,
        n: i32,
        base: u32,
        ctx: &mut dyn ConsCtx
    ) -> Result<Option<TermId>, Error>;
fn dyn_has_var_dep(&self, ix: u32, equiv: bool) -> bool;
fn dyn_has_dep_below(&self, ix: u32, base: u32) -> bool;
fn dyn_load_flags(&self) -> TyckFlags;
fn dyn_set_flags(&self, flags: TyckFlags);
fn dyn_eq_in(
        &self,
        other: &dyn DynamicValue,
        ctx: &mut dyn TermEqCtxMut
    ) -> Option<bool>;
fn as_any(&self) -> &dyn Any; fn dyn_eq_term_in(
        &self,
        other: &Term,
        ctx: &mut dyn TermEqCtxMut
    ) -> Option<bool> { ... }
fn dyn_eq_id_in(
        &self,
        other: &TermId,
        ctx: &mut dyn TermEqCtxMut
    ) -> Option<bool> { ... }
}
Expand description

The interface which must be implemented by dynamic terms

Rather than implement this manually, it is usually preferable to implement Value, which will implement this trait automatically assuming the type also satisfies Debug, Hash, PartialEq, and 'static.

Required methods

Cons this term within a given context. Return None if already consed.

Get the type annotation of this term

Get the index of this term in an isotope program graph, if any

Get the hash-code of this term

Get whether this term is a type

Get whether this term is a universe

Get whether this term is in “root form”

Get whether this term is a subtype of another term in a given context

Get whether this term has a universe in all contexts

Get the untyped hash-code of this term

Get the variable filter of this term

Shift this term’s variables with index >= base up by n in a given context

Whether this term has a given variable dependency

Whether this term has a given variable dependency below ix and above base

Load this term’s flags

Set this term’s flags

Compare this term to another dynamic term

Convert this term to an Any

Provided methods

Compare this term to another

Compare this term to a term ID

Implementors